Definitions	False, P Q, A, A B, t T, x:A. B(x), , S T, ,
Lemmas	nat plus wf, le wf